(set-logic QF_LRA)
(declare-fun _substvar_38_ () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(assert (distinct v2 v4))
(assert (xor v5 v4))
(assert (= (and v3 (xor v5 (distinct v2 v4))) _substvar_38_))
(assert v3)
(check-sat)
(assert (distinct v4 (and (distinct v2 v4) v4)))
(push 1)
(check-sat)
(pop 1)
(check-sat)
